;;;============================================================
;;;
;;; Subject: Equivalence between cmp-d-ls-d-do and 
;;;          1dlop-dgop-d-do
;;;         
;;;
;;;------------------------------------------------------------
;;;
;;;
;;;============================================================

#| Certification code:

(certify-book "1dlop-dgop-do-cmp-d-ls-d-do" 0 nil)

|#


(in-package "ACL2")


;;;------------------------------------------------------------
;;;
;;; EAT representation
;;;
;;;------------------------------------------------------------

(include-book "dg-list")

(defun cmp-d-ls-dgop-do (d p rsl)
  (cond ((endp p) (reverse rsl))
        ((< d (car p)) (cmp-d-ls-dgop-do d (cdr p) (cons (1- (car p)) rsl)))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) (append (reverse rsl) (rest p)))
        (t (cmp-d-ls-dgop-do (1- d) (cdr p) (cons (car p) rsl)))
        )
  )

(defun cmp-d-ls-d-do (d p)
  (cond ((endp p) d)
	((< d (car p)) (cmp-d-ls-d-do d (cdr p) ))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) nil)
        (t (cmp-d-ls-d-do (1- d) (cdr p)))
        )
  )

(defun cmp-d-ls (d ls)
  (cmp-d-ls-dgop-do d ls nil)
  )


(encapsulate
 ()
 
 (local
  (defthm append-revappend
      (equal (append (revappend l1 l2) l3)
             (revappend l1 (append l2 l3)))))
 
 (local
  (defthm revappend-append
      (equal (revappend (append ls1 ls2) ls3)
             (revappend ls2 (revappend ls1 ls3)))))
 
 (local
  (defthm cmp-d-ls-dgop-do-append-rsl
      (implies (and (true-listp rsl1)
                    (true-listp rsl2))
               (equal (cmp-d-ls-dgop-do s p (append rsl1 rsl2))
                      (append (reverse rsl2) (cmp-d-ls-dgop-do s p rsl1))))
    :rule-classes nil))
 
 (local
  (defthm cmp-d-ls-dgop-do-nil-rsl
      (implies (and (true-listp rsl1)
                    (not (endp rsl1)))
               (equal (cmp-d-ls-dgop-do s p rsl1)
                      (append (reverse rsl1) (cmp-d-ls-dgop-do s p nil))))
    :hints (("Goal" :use (:instance cmp-d-ls-dgop-do-append-rsl
                                    (rsl1 nil)
                                    (rsl2 rsl1))))))
 
 (defthm cmp-d-ls-recursive
     (equal (cmp-d-ls d ls)
            (cond ((endp ls) nil)
                  ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls d (cdr ls))))
                  ((and (<= 0 (- d (car ls)))
                        (<= (- d (car ls)) 1)) (cdr ls))              
                  (t (cons (car ls) (cmp-d-ls (1- d) (cdr ls))))
                  ))
   :rule-classes :definition)
 
 (defun cmp-d-ls-induct (d ls)
   (cond 
	 ((endp ls) nil)
         ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls-induct d (cdr ls))))
         ((and (<= 0 (- d (car ls)))
               (<= (- d (car ls)) 1)) (cdr ls))              
         (t (cons (car ls) (cmp-d-ls-induct (- d 1) (cdr ls))))
         )
   )
 
 (in-theory (disable cmp-d-ls))
 
 )

(defthm cmp-d-ls-cmp-d-ls-induct
    (equal (cmp-d-ls i ls)
           (cmp-d-ls-induct i ls)))

;; Notar que si > j (1+ (car ls)) entonces cmp-d-ls-induct j ls es ls

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1-bis
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2-bis
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm dgl-p-cmp-d-ls
    (implies (and (dgl-p dgl)
                  (natp n))
             (dgl-p (cmp-d-ls n dgl)))
  :hints (("Goal" :induct (cmp-d-ls-induct n dgl))))

(defthm cmp-d-ls-d-do-not-nil
  (implies (and (natp j) 
		(dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (cmp-d-ls-d-do j ls)))




(defun remove-from (i ls)
  (cond ((endp ls) nil)
	((= i (car ls)) (cdr ls))
	((> i (car ls)) ls)
	(t (remove-from i (cdr ls)))))


(defun right-count (i ls)
  (- i (len(remove-from i ls))))


(defthm cmp-d-ls-d-do-right-count
  (implies (and (natp i)
		(dgl-p ls)
		(cmp-d-ls-d-do i ls))
	   (equal (cmp-d-ls-d-do i ls)
		  (right-count i ls))))


(defun new-cmp-d-ls-d-do (i ls)
  (if (cmp-d-ls-d-do i ls)
      (right-count i ls)
    nil))


(defthm equal-new-and-old
  (implies (and (natp i)
		(dgl-p ls))
	   (equal (new-cmp-d-ls-d-do i ls)
		  (cmp-d-ls-d-do i ls))))


;;;------------------------------------------------------------
;;;
;;; Binary representation
;;;
;;;------------------------------------------------------------


(include-book "dg-binary")


(defun remove-from-binary (i ls)
  (cond ((endp ls) nil)
	((zp i) nil)
	(t (cons (car ls) (remove-from-binary (- i 1) (cdr ls)))
)))


(defthm remove-from-0
  (implies (dgl-p dgl)
	   (equal (remove-from 0 dgl)
		  nil)))

(defthm dgl-p-append-1+ls-dgop-0
  (implies (dgl-p dgop)
	   (dgl-p (append (1+ls dgop) '(0)))))

(defthm dgl-p-append-1+ls
  (implies (dgb-p dgb)
	   (dgl-p (append (1+ls (dgb->dgl dgb))
			  '(0)))))

(defthm dgl-p-1+ls-dgl
  (implies (dgl-p dgb)
	   (dgl-p (1+ls dgb))))


(defthm dgl-p-1+ls-dgb
  (implies (dgb-p dgb)
	   (dgl-p (1+ls (dgb->dgl dgb))
			  )))



(defthm remove-1+ls
  (implies (and (natp i)
		(not (zp i))
		(dgl-p dgl))
	   (equal (append (1+ls (remove-from (+ -1 i) dgl)) '(0))
		  (remove-from i (append (1+ls dgl) '(0))))))


(defthm remove-1+ls-2
  (implies (and (natp i)
		(not (zp i))
		(dgl-p dgl))
	   (equal (1+ls (remove-from (+ -1 i) dgl))
		  (remove-from i (1+ls dgl)))))
		  


(defthm remove-from-binary=remove-from
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (dgb->dgl (remove-from-binary i dgb))
		  (remove-from i (dgb->dgl dgb)))))


(defthm remove-from-binary=remove-from
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (dgb->dgl (remove-from-binary i dgb))
		  (remove-from i (dgb->dgl dgb)))))



(include-book "binary-remove-zeros")


(defthm remove-from-binary=remove-from-dgl->dgb
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (dgl->dgb (dgb->dgl (remove-from-binary i dgb)))
		  (dgl->dgb (remove-from i (dgb->dgl dgb))))))


(defthm quasi-dgb-p-remove-from-binary
  (implies (and (natp i)
		(dgb-p dgb))
	   (quasi-dgb-p (remove-from-binary i dgb))))


(defun final-remove-from-binary (i ls)
  (remove-final-zeros (remove-from-binary i ls)))


(defthm remove-binary=remove-from-A
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (dgl->dgb (dgb->dgl (remove-final-zeros
			     (remove-from-binary i dgb))))
		  (dgl->dgb (remove-from i (dgb->dgl dgb)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-from-binary=remove-from-dgl->dgb)
		 (:instance dgb->dgl-remove-final-zeros
			    (dgop (remove-from-binary i dgb))))))
)


(defthm remove-binary=remove-from-B
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (remove-final-zeros
			     (remove-from-binary i dgb))
		  (dgl->dgb (remove-from i (dgb->dgl dgb)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-binary=remove-from-A)
		 (:instance quasi-dgb-p-remove-from-binary)
		 (:instance quasi-dgb-to-dgb
			    (dgb (remove-from-binary i dgb)))
		 (:instance dgl->dgb-dgb->dgl
			    (dgb (remove-final-zeros
			     (remove-from-binary i dgb))))
			    ))))

(defthm final-remove-binary-is-equal-to-remove-from
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (final-remove-from-binary i dgb)
		  (dgl->dgb (remove-from i (dgb->dgl dgb)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-binary=remove-from-B)))))

(defthm final-remove-binary-is-equal-to-remove-from-2
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (dgb->dgl (final-remove-from-binary i dgb))
		  (dgb->dgl (dgl->dgb (remove-from i (dgb->dgl dgb))))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-remove-from)))))

(defthm dgl-p-remove-from
  (implies (and (natp i)
		(dgl-p dgl))
	   (dgl-p (remove-from i dgl))))

(defthm final-remove-binary-is-equal-to-remove-from-3
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (dgb->dgl (final-remove-from-binary i dgb))
		  (remove-from i (dgb->dgl dgb))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-remove-from-2)
		 (:instance dgl-p-remove-from
			    (dgl (dgb->dgl dgb)))
		 (:instance dgb->dgl-dgl->dgb
			    (dgl (remove-from i (dgb->dgl dgb))))))))
     

(defun len-count (dgb)
  (if (endp dgb)
      0
    (if (equal (car dgb) 1)
	(+ 1 (len-count (cdr dgb)))
      (len-count (cdr dgb)))))  

(defthm len-count=len
  (implies (and (equal (len-count dgop) n) (dgb-p dgop))
	   (equal (len (dgb->dgl dgop)) n)
	   ))

(defthm len-count-is-equal-len
  (implies (and (dgb-p dgop))
	   (equal (len-count dgop)
		  (len (dgb->dgl dgop)))
	   ))

(defun right-count-binary (i ls)
  (- i (len-count (final-remove-from-binary i ls))))


(defthm len-count-binary=len-count
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (len-count (final-remove-from-binary i dgb))
		  (len (remove-from i (dgb->dgl dgb)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-remove-from-3)
		 (:instance len-count-is-equal-len
			    (dgop (final-remove-from-binary i dgb))
			    )))))


(defthm right-count-binary=right-count
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (right-count-binary i (final-remove-from-binary i dgb))
		  (right-count i (remove-from i (dgb->dgl dgb)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-remove-from-3)
		 (:instance len-count-is-equal-len
			    (dgop (final-remove-from-binary i dgb))
			    )))))


(include-book "my-logbitp")


(defun real-1dlop-dgop-d-do-binary (d dgop)
  (if (1dlop-dgop-binary-do d dgop)
      nil
    (right-count-binary d dgop)))


(defthm equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-a
  (implies (and (natp i)
		(dgb-p dgb)
		(1dlop-dgop-binary-do i dgb)
		(null (cmp-d-ls-d-do i (dgb->dgl dgb))))
	   (equal (real-1dlop-dgop-d-do-binary i dgb)
		  (new-cmp-d-ls-d-do i (dgb->dgl dgb)))))


(defthm equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-b
  (implies (and (natp i)
		(dgb-p dgb)
		(1dlop-dgop-binary-do i dgb))
	   (equal (real-1dlop-dgop-d-do-binary i dgb)
		  (new-cmp-d-ls-d-do i (dgb->dgl dgb))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop-binary-do-implies-null-cmp-d-ls-d-do
			  (d i))
	       (:instance  equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-a)))))

(defthm equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-c
  (implies (and (natp i)
		(dgb-p dgb)
		(null (1dlop-dgop-binary-do i dgb))
		(cmp-d-ls-d-do i (dgb->dgl dgb)))
	   (equal (real-1dlop-dgop-d-do-binary i dgb)
		  (new-cmp-d-ls-d-do i (dgb->dgl dgb)))))

(defthm equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-d
  (implies (and (natp i)
		(dgb-p dgb)
		(null (1dlop-dgop-binary-do i dgb)))
	   (equal (real-1dlop-dgop-d-do-binary i dgb)
		  (new-cmp-d-ls-d-do i (dgb->dgl dgb)))))


(defthm equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (real-1dlop-dgop-d-do-binary i dgb)
		  (new-cmp-d-ls-d-do i (dgb->dgl dgb))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance  equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-b)
	       (:instance  equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-d)))))

    
(defthm equal-real-1dlop-dgop-d-do-binary-and-cmp-d-ls-d
  (implies (and (natp i)
		(dgb-p dgb))
	   (equal (real-1dlop-dgop-d-do-binary i dgb)
		  (cmp-d-ls-d-do i (dgb->dgl dgb)))))



;;;------------------------------------------------------------
;;;
;;; Kenzo representation
;;;
;;;------------------------------------------------------------

(include-book "dg-natural")

(include-book "arithmetic-4/top" :dir :system)

(defun right (1dlop dgop)
  (logandc1 (ash -1 1dlop) dgop))


(defthm equal-0=>nil-or-all-zeros
  (implies (and (quasi-dgb-p dgop)
		(equal 0 (dgb->dgn dgop)))
	   (or (equal nil dgop)
	       (all-zeros-p dgop)))
  :rule-classes nil)

(defun remove-from-binary=right-schema1 (i dgop)
  (declare (xargs :measure (len dgop)))
  (if (or (not (natp i))
	  (not (dgb-p dgop)))
      nil
    (if (endp dgop)
	0
      (+ (car dgop) (ash (remove-from-binary=right-schema1 (- i 1) (cdr dgop))
			 1)))))


(defthm remove-from-binary-right-1
  (implies (and (not (cdr dgop))
		(consp dgop)
		(integerp i)
		(<= 1 i))
	   (equal (remove-from-binary i dgop)
		  dgop)))

(defthm commutative-logand
    (equal (logand a b) (logand b a)))


(defthm not-zp-i-expt
  (implies (not (zp i))
	   (integerp (expt 2 i))))

(defthm not-zp-i-expt-
  (implies (not (zp i))
	   (integerp (- (expt 2 i)))))

(defthm lognot-property-1
  (implies (integerp a)
	   (equal (lognot a)
		  (+ (- (ifix a)) -1)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance lognot (i a))))))

(defthm lognot-property-2
  (implies (integerp a)
	   (equal (lognot a)
		  (+ (- a) -1)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance lognot (i a))))))


(defthm lognot-expt
  (implies (and (not (zp i))
		(<= 0 i))
	   (equal (- (expt 2 i) 1)
		  (lognot (- (expt 2 i)))
		  )))

(in-theory (disable lognot-expt lognot-property-2
		    lognot-property-1))



(defthm evenp-expt
  (implies (and (not (zp i))
		(<= 0 i))
	   (evenp (expt 2 i)))
  :hints (("Goal" :in-theory (enable expt evenp))))



(defthm not-evenp-expt
  (implies (and (not (zp i))
		(<= 0 i))
	   (not (evenp (- (expt 2 i) 1))))
  :hints (("Goal" :in-theory (enable expt evenp))))

(defthm not-evenp-expt-2
  (implies (and (not (zp i))
		(<= 0 i))
	   (not (evenp (+ -1 (* 2 (expt 2 (+ -1 i)))))))
  :hints (("Goal" :in-theory (enable expt evenp))))

(defthm remove-from-binary=right
  (implies (and (natp i)
		(dgb-p dgop))
	   (equal (dgb->dgn (remove-from-binary i dgop))
		  (right i (dgb->dgn dgop))
		  ))
  :hints (("Goal" :in-theory (enable logand ash lognot expt evenp)
	   :induct (remove-from-binary=right-schema1 i dgop))))


(defthm remove-from-binary=right-a
  (implies (and (natp i)
		(dgb-p dgop))
	   (equal (dgn->dgb (dgb->dgn (remove-from-binary i dgop)))
		  (dgn->dgb (right i (dgb->dgn dgop)))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-from-binary=right)))))


(include-book "kenzo-remove-zeros")


(defthm remove-from-binary=right-b
  (implies (and (natp i)
		(dgb-p dgop))
	   (equal (dgn->dgb (dgb->dgn (remove-final-zeros
			     (remove-from-binary i dgop))))
		  (dgn->dgb (right i (dgb->dgn dgop)))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-from-binary=right-a)
		 (:instance dgb->dgn-remove-final-zeros
			    (dgop (remove-from-binary i dgop))))))
)


(defthm remove-from-binary=right-c
  (implies (and (natp i)
		(dgb-p dgop))
	   (equal (remove-final-zeros
			     (remove-from-binary i dgop))
		  (dgn->dgb (right i (dgb->dgn dgop)))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-from-binary=right-b)
		 (:instance quasi-dgb-p-remove-from-binary
			    (dgb dgop))
		 (:instance quasi-dgb-to-dgb
			    (dgb (remove-from-binary i dgop)))
		 (:instance dgn->dgb-dgb->dgn
			    (dgb (remove-final-zeros
			     (remove-from-binary i dgop))))
			    ))))

(defthm final-remove-binary-is-equal-to-right
  (implies (and (natp i)
		(dgb-p dgop))
	   (equal (final-remove-from-binary i dgop)
		  (dgn->dgb (right i (dgb->dgn dgop)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-from-binary=right-c)))))

(defthm final-remove-binary-is-equal-to-right-inverse-aux
  (implies (and (natp i)
		(natp dgop))
	   (equal (final-remove-from-binary i (dgn->dgb dgop))
		  (dgn->dgb (right i dgop))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-right
			    (dgop (dgn->dgb dgop)))))))


(defthm final-remove-binary-is-equal-to-right-inverse
  (implies (and (natp i)
		(natp dgop))
	   (equal (dgb->dgn (final-remove-from-binary i (dgn->dgb dgop)))
		  (right i dgop)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable final-remove-from-binary)
	   :use ((:instance final-remove-binary-is-equal-to-right-inverse-aux
			    )))))


(defthm remove-from-is-equal-to-right
  (implies (and (natp i)
		(natp dgop))
	   (equal (right i dgop)
		  (dgb->dgn (dgl->dgb (remove-from i (dgb->dgl (dgn->dgb dgop))))
		  )))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-right-inverse)
		 (:instance final-remove-binary-is-equal-to-remove-from
			    (dgb (dgn->dgb dgop)))))))

(defthm remove-from-is-equal-to-right-2
  (implies (and (natp i)
		(natp dgop))
	   (equal (right i dgop)
		  (dgop-ext-int (remove-from i (dgop-int-ext dgop))
		  )))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance remove-from-is-equal-to-right)
		 ))))


(defun right-count-kenzo (i ls)
  (- i (logcount (right i ls))))


(defthm floor-nonnegative-integer-quotient
  (implies (not (zp n))
	   (equal (nonnegative-integer-quotient n 2)
		  (floor n 2)))
  )

(defthm logcount-ash
  (implies (and (not (zp n))
		(evenp n))
	   (equal (logcount (ash n -1))
		  (logcount n)
		))
:hints (("Goal" :in-theory (enable logcount ash evenp))))

(defthm logcount-floor
  (implies (and (not (zp n))
		(evenp n))
	   (equal (logcount (floor n 2))
		  (logcount n)
		))
:hints (("Goal" :in-theory (enable logcount floor evenp)))
)

(defthm logcount=len-count-1
  (implies (natp dgop)
	   (equal (len-count (dgn->dgb dgop))
		(logcount dgop)
		))
:hints (("Goal" :in-theory (enable logcount floor evenp ash)))
)


(defthm len-count-binary=logcount
  (implies (and (natp i)
		(natp dgop))
	   (equal (logcount (right i dgop))
		  (len-count (final-remove-from-binary i (dgn->dgb dgop)))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance final-remove-binary-is-equal-to-right-inverse-aux)
		 (:instance logcount=len-count-1
			    (dgop (right i dgop))
			    )))))

(defthm len=logcount
  (implies (and (natp i)
		(natp dgop))
	   (equal (logcount (right i dgop))
		  (len (remove-from i (dgb->dgl (dgn->dgb dgop))))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance len-count-binary=logcount)
		 (:instance len-count-binary=len-count
			    (dgb (dgn->dgb dgop))
			    )))))

(defthm len=logcount-1
  (implies (and (natp i)
		(natp dgop))
	   (equal (logcount (right i dgop))
		  (len (remove-from i (dgop-int-ext dgop)))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance len=logcount)
		 ))))

(defthm right-count-binary=right-count-kenzo-aux
  (implies (and (natp i)
		(natp dgop))
	   (equal (- i (logcount (right i dgop)))
		  (- i (len-count (final-remove-from-binary i (dgn->dgb dgop))))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance len-count-binary=logcount
			    )))))


(defthm right-count-binary=right-count-kenzo
  (implies (and (natp i)
		(natp dgop))
	   (equal (right-count-kenzo i dgop)
		  (right-count-binary i (dgn->dgb dgop))
		  ))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable right final-remove-from-binary)
	   :use ((:instance right-count-binary=right-count-kenzo-aux
			    )))))

(defthm right-count=right-count-kenzo
  (implies (and (natp i)
		(natp dgop))
	   (equal (right-count-kenzo i dgop)
		  (right-count i (dgb->dgl (dgn->dgb dgop)))
		  ))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable right final-remove-from-binary)
	   :use ((:instance right-count-binary=right-count-kenzo
			    )))))

(defthm right-count=right-count-kenzo-1
  (implies (and (natp i)
		(natp dgop))
	   (equal (right-count-kenzo i dgop)
		  (right-count i (dgop-int-ext dgop))
		  ))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable right final-remove-from-binary)
	   :use ((:instance right-count=right-count-kenzo
			    )))))


(include-book "logbitp")


(defun real-1dlop-dgop-do (d dgop)
  (if (1dlop-dgop-do d dgop)
      nil
    (right-count-kenzo d dgop)))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-a
  (implies (and (natp i)
		(natp dgop)
		(1dlop-dgop-do i dgop)
		(null (cmp-d-ls-d-do i (dgop-int-ext dgop))))
	   (equal (real-1dlop-dgop-do i dgop)
		  (new-cmp-d-ls-d-do i (dgop-int-ext dgop)))))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-b
  (implies (and (natp i)
		(dgb-p dgop)
		(1dlop-dgop-do i dgop))
	   (equal (real-1dlop-dgop-do i dgop)
		  (new-cmp-d-ls-d-do i (dgop-int-ext dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop-do=1dlop-dgop-binary-do (d i))
	       (:instance equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-a
			  (dgb (dgn->dgb dgop)))))))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-1
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-do i dgop))
		(null (1dlop-dgop-binary-do i (dgn->dgb dgop))))
	   (equal (real-1dlop-dgop-do i dgop)
		  (real-1dlop-dgop-d-do-binary i (dgn->dgb dgop))
		  )))

(defthm null-1dlop-dgop-do=1dlop-dgop-binary-do
  (implies (and (natp d)
		(natp dgop)
		(null (1dlop-dgop-do d dgop)))
	  (null (1dlop-dgop-binary-do d (dgn->dgb dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-do 1dlop-dgop-binary-do)
	 :use ((:instance 1dlop-dgop-do=1dlop-dgop-binary-do)
	       ))))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-2
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-do i dgop))
		)
	   (equal (real-1dlop-dgop-do i dgop)
		  (real-1dlop-dgop-d-do-binary i (dgn->dgb dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do real-1dlop-dgop-d-do-binary)
	 :use ((:instance null-1dlop-dgop-do=1dlop-dgop-binary-do (d i))
	       (:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-1
	       )))))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-3
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-binary-do i (dgn->dgb dgop)))
		(cmp-d-ls-d-do i (dgb->dgl (dgn->dgb dgop)))
		)
	   (equal (real-1dlop-dgop-d-do-binary i (dgn->dgb dgop))
		  (new-cmp-d-ls-d-do i (dgb->dgl (dgn->dgb dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do real-1dlop-dgop-d-do-binary)
	 :use ((:instance equal-real-1dlop-dgop-d-do-binary-and-new-cmp-d-ls-d-c
			  (dgb (dgn->dgb dgop)))))))

(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-4
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-do i dgop))
		(cmp-d-ls-d-do i (dgb->dgl (dgn->dgb dgop)))
		)
	   (equal (real-1dlop-dgop-d-do-binary i (dgn->dgb dgop))
		  (new-cmp-d-ls-d-do i (dgb->dgl (dgn->dgb dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do real-1dlop-dgop-d-do-binary)
	 :use ((:instance null-1dlop-dgop-do=1dlop-dgop-binary-do (d i)
			  (dgop (dgn->dgb dgop)))
	       (:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-3))
	 )))

(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-do i dgop))
		(cmp-d-ls-d-do i (dgb->dgl (dgn->dgb dgop)))
		)
	   (equal (real-1dlop-dgop-do i dgop)
		  (new-cmp-d-ls-d-do i (dgb->dgl (dgn->dgb dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do 
			     1dlop-dgop-do
			     new-cmp-d-ls-d-do cmp-d-ls-d-do
			     real-1dlop-dgop-d-do-binary)
	 :use ((:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-2)
	       (:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c-4))
	 )))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c0
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-do i dgop))
		(cmp-d-ls-d-do i (dgop-int-ext dgop))
		)
	   (equal (real-1dlop-dgop-do i dgop)
		  (new-cmp-d-ls-d-do i (dgop-int-ext dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do 
			     1dlop-dgop-do
			     new-cmp-d-ls-d-do cmp-d-ls-d-do
			     real-1dlop-dgop-d-do-binary)
	 :use ((:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c)
	       )
	 )))


(defthm null=>cmp-d-ls-d-o
  (implies (and (natp i)
		(dgb-p dgop)
		(null (1dlop-dgop-do i dgop)))
	   (cmp-d-ls-d-do i (dgop-int-ext dgop))))



(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-d
  (implies (and (natp i)
		(natp dgop)
		(null (1dlop-dgop-do i dgop)))
	   (equal (real-1dlop-dgop-do i dgop)
		  (new-cmp-d-ls-d-do i (dgop-int-ext dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do 
			     1dlop-dgop-do
			     cmp-d-ls-d-do
			     new-cmp-d-ls-d-do cmp-d-ls-d-do
			     real-1dlop-dgop-d-do-binary)
	 :use ((:instance null=>cmp-d-ls-d-o)
	       (:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-c0
			  )))))


(defthm equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d
  (implies (and (natp i)
		(natp dgop))
	   (equal (real-1dlop-dgop-do i dgop)
		  (new-cmp-d-ls-d-do i (dgop-int-ext dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do 
			     1dlop-dgop-do
			     cmp-d-ls-d-do
			     new-cmp-d-ls-d-do cmp-d-ls-d-do
			     real-1dlop-dgop-d-do-binary)
	 :use ((:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-b)
	       (:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-d)))))


(defthm equal-real-1dlop-dgop-do-and-cmp-d-ls-d
  (implies (and (natp i)
		(natp dgop))
	   (equal (real-1dlop-dgop-do i dgop)
		  (cmp-d-ls-d-do i (dgop-int-ext dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable real-1dlop-dgop-do 
			     1dlop-dgop-do
			     cmp-d-ls-d-do
			     new-cmp-d-ls-d-do cmp-d-ls-d-do
			     real-1dlop-dgop-d-do-binary)
	 :use ((:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-b)
	       (:instance equal-real-1dlop-dgop-do-and-new-cmp-d-ls-d-d)))))
